T:Type, dT:EqDecider(T), L:T List, x, y:T.
(x  L)  (y  L)  index(L;x)index(L;y)  x before y  L  x = y 

latex

Definitions	P  Q, P  Q, T, True, P & Q, l[i], index(L;x), A, False, AB, (x  l), EqDecider(T), Dec(P), P  Q, {T}, P  Q, {i..j}, ||as||, Prop, t  T, x before y  l, x:A. B(x)
Lemmas	l before wf, length wf1, int seg wf, l index wf, decidable lt, deq wf, l member wf, le wf, l before l index, squash wf, select wf, select l index